mcsta/modest mcsta crowds.jani -E TotalRuns=5,CrowdSize=20 --props positive -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 1e-6 --width 1e-6 --relative-width --p0 --p1
crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 40 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 2018094 states for TotalRuns=5, CrowdSize=20.
Peak memory usage: 687 MB
Analysis results for crowds.jani
Experiment TotalRuns=5, CrowdSize=20
+ State space exploration
State size: 40 bytes
States: 2018094
Transitions: 2018094
Branches: 7224834
Rate: 396015 states/s
Time: 5.4 s
+ Property positive
Probability: 0.08606910446098197
Bounds: [0.08606904815340224, 0.08606916076856169]
Time: 1.8 s
+ Precomputations
Min. prob. 0 states: 1745849
Time for min. prob. 0 states: 0.5 s
Min. prob. 1 states: 3542
Time for min. prob. 1 states: 0.1 s
+ Essential states
Iterations: 2
Essential states: 212522
Transitions: 212522
Branches: 1700162
Time: 0.2 s
+ Optimistic value iteration
Total iterations: 70
Verif. attempts: 2
Verif. iterations: 8
Final epsilon: 1.2125355883762495E-07
Time: 0.9 s
Exported results to file "/out.txt".